Nuprl Lemma : es-real-implies 0,22

P:(ES{i}Prop{i'}), p:es-real{i:l}(es.P(es)), es:ES{i}.
Consistent(es-realizer(p);es P(es
latex


Definitionst  T, P  Q, x:AB(x), es-realizer(p), x:AB(x), P & Q, R ||- es.P(es), x:AB(x), es.P(es), Type, Prop, ES, x:AB(x), f(a), x(s), xt(x), x.A(x), Consistent(R;es)
LemmasR-consistent wf, es-realizer wf, es-real wf, event system wf

origin